Multiversion Concurrency Control - Theory and Algorithms
Reference
Philip A. Bernstein and Nathan Goodman. 1983. Multiversion concurrency control—theory and algorithms. ACM Trans. Database Syst. 8, 4 (December 1983), 465-483. DOI=http://dx.doi.org/10.1145/319996.319998 論文の意義
この論文で初出となった概念を挙げると
1. Introduction
When transactions execute concurrently, the interleaved execution of their reads and writes by the DBS can produce undesirable results.
Concurrency Control is the activity of avoiding such undesirable results.
Specifically, the goal of concurrency control is to produce an execution that has the same effect as a serial(noninterleaved) one. Such executions are called Serializable. DBS = database systems = DBMS = DBぐらいで読み替えてよし.
MVCCでは,1VCCだと間違いなくAbortするような状況でも,Commitできる場合がある. たとえば,
code: multiversion read.cpp
T0.write(x,0)
T1.read(x) # => 0
T2.write(x, 2)
T3.read(x) # => 0
というふうに,$ T_3が古い値を読んでしまった場合,従来の考え方だと「まずそう」なわけだが,
$ T_1 \to T_3 \to T_2の順番のnoninterleaved executionとおそらくsame effectになるだろう.
ということで,この論文は,MVCCの理論的な基礎づけを行っている.
2.Basic Serializability Theory
この論文時点でStandardであった,過去の(つまり1VCCの)Serializability Theoryについて説明している. 要点を抜粋すると,Formalに重要なのは以下.
Formally, a transaction log is a partially ordered set(poset) $ T_i = (\Sigma_i, <_i) where $ \Sigma_i is the set of reads and writes issued by (an execution of) transaction $ i, and $ <_i tells the order in which those operations must be executed. ... Let $ T = \{T_0, ..., T_n \} be a set of transaction logs. ... Formally, a log over $ T is a poset $ L = (\Sigma, <), where
(1) $ \Sigma = \cup^n_{i=0} \Sigma_i;
(2) $ < \subseteq \cup^n_{i=0} <_i;
(3) every $ r_j(x) is preceded by at least one $ w_i(x)($ i= jis possible), where $ w_i(x)precedes $ r_j(x) is synonymous with $ w_i(x) < r_j(x);
(4) all pairs of conflicting operations are $ <related (two operations $ conflict if they operate on the same data item, and at least one is a write).
Transaction Log: トランザクションはread/write命令を元とする半順序集合である.
$ T: トランザクションの集合.
$ L: ログ.これによって,$ Tが実行されたデータベース全体を示す.より具体的には:
(1) 全トランザクションの命令の和集合$ \Sigmaをもっている
(2) 各トランザクションの命令順序を全て保存(order-preserving)している順序和集合$ <をもっている
(4) $ <は,トランザクション間であっても,conflictな2つの命令間では,順序をもつ
conflict: 同じタプルについての2命令間の関係.writeを一つでも含むならconflict.
ワカっている人は「ログ」を「ヒストリ」に読み替えると話が早い.
Equivalence
等価性があれば,「2つのログが等価である($ L_1 \equiv L_2)」といえる.
このうち片方のログが直列実行(noninterleaved)のものなら,1. で示したSerializableは,「ログが等価であればSerializable」と具体的に定義できる. 以下に要点を抜粋.
Transaction $ T_jreads-x-from $ T_iin $ L if
(1) $ w_i(x) and $ r_j(x) are operations in $ L.
(2) $ w_i(x) < r_j(x);
(3) no $ w_k(x)falls between these operations.
Two logs over $ \{T_0, ..., T_n\}are $ equivalent, denoted $ \equiv, if they have the same reads-from relationships; that is, for all $ i,j,and $ x,$ T_j reads-x-from $ T_i in one log iff this condition holds in the other.
つまり,「ある値をAが書いた」「その後Bが読んだ」という構造を抜き出して,これが全て同じなら,2つのログは等価である,とする.
このあたりはReads-Fromに詳しい.以降は,この関係性を$ \{(T_i, x, T_j)\}と表記する. ということは,以下も真:
For example, the logs:
$ L = w_0(x) w_1(x) and $ L' = w_1(x)w_0(x)
are equivalent, even though different transactions produce the final value of $ x in each log.
データベースの最終状態が何であろうと,読み込みさえうまくいっていればよい,ということになる.
このあと$ r_2(x)が来れば,$ L \neq L'になる.
" $ w_i(x)and $ r_j(x) are operations in $ Lover $ T \cup \{T_\infty\}"みたいな感じにすればいい
Final Transaction: データベースの全てのタプルを読む,最後のトランザクション.
Serializability
Equivalenceを使って,Serializabilityを定義する.
まず,直列実行した際のログをserial logとする.
A $ serial\ logis a totally ordered log on $ \Sigma such that for every pair of transactions $ T_iand $ T_j, either all the operations of $ T_iprecede all those of $ T_j, or vice versa.
このserial logと等価(equivalent)なログをserializable(SR)とすればいい.
つまり以下が,過去のSerializabilityの定理である.
Let $ L be a log over $ \{T_0, ..., T_n \}. The $ serialization\ graph for $ L, $ SG(L), is a directed graph whose nodes are $ T_0, ..., T_n,and whose edges are all $ T_i \to T_j (i\ne j)such that some operation of $ T_iprecedes and conflicts with some operation of $ T_j.
SERIALIZABILITY THEOREM(4, 8, 14, 16, 21). If $ SG(L) is acyclic, then $ L is $ SR.
Proofは過去の論文たちによってされているが,同じReads-Fromであれば,Conflictの順序が同じになる.
ので,Conflictでグラフを描いて,トポロジカルソート可能なら,Serializable,となる.
ここからは,マルチバージョンのSerializabilityを定式化していく.
3. Multiversion Serializability Theory
まず,Read/Write Operationのnotationを拡張する.
We denote versions of $ x by $ x_i, x_j, ...,where the subscript is the index of the transaction that wrote the version.
Operations on versions are denoted $ r_i(x_j) and $ w_i(x_i).
これまでのnotationは$ r_i(x), w_i(x)だったので,暗に「最新を読む」「上書き」を意味していたことに.
次に,このバージョンを与える関数を定義する.(同時に,これで,マルチバージョンのログも定義できる)
We formalize this translation by a function $ hwhich maps each $ w_i(x) into $ w_j(x_i), and each $ r_i(x) into $ r_i(x_j) for some $ j.
A multiversion DBS log (or simply MV log) over $ Tis a poset $ L = (\Sigma, <) where
(1) $ \Sigma=h(\cup^n_{i=1}\Sigma_i) for some translation function$ h.
(2) for each $ T_iand all operations $ op_iand $ op_i',if $ op_i <_i op_i'then $ h(op_i) < h(op_i'), and
(3) if $ h(r_j(x)) = r_j(x_i)then $ w_i(x_i) < r_j(x_i).
同じトランザクション集合$ Tについて,半順序集合$ Lは,
(2): 同じトランザクション内で先に実行されている命令には,先に$ hを適用する
$ h(op_i) < h(op_i')の意味するところ(何を比較?)が若干わからないが,おそらくこれ
多分,$ r_i(x)w_i(x)を$ r_i(x_i)w_i(x_i)としてしまうのを避けたいんだろう.
(3) $ hによってreadに付与しうるVersionは,必ずログ上の順序$ <において先行するものだけ.
MV Equivalence(Reads-From)
さて,2. のBasic Serializability Theoryで論じた多くの定義が,MVのSerializability Theoryでも流用できる.
単に s/data item/version とすればよいだけ.
改めてMVにおけるSerializability Theoryを述べると:
Let $ L be an MV log over $ \{T_0, ..., T_n\}. Transaction $ T_jreads-x-from $ T_i in $ L if $ T_j reads the version of $ x produced by $ T_i. By definition, the version of $ x produced by $ T_i is $ x_i.
This means that the reads-from relationships in $ L are determined by the translation function $ h, namely, by the way $ htranslates "data item reads" into "version reads".
$ r_i(x_j)のとき,Reads-Fromは$ \{(T_j, x, T_i)\}になる..ということは, Monoversionでは「命令の順序$ <」がReads-Fromを決めていたが,
Multiversionでは,Version Function$ hがReads-Fromを決めることになる.
つまり,順序ではなくread命令の添字(version subscript)だけでReads-Fromが作れるのだから,以下がいえる
FACT 1. Two MV logs over a set of transactions $ Tare equivalent iff the logs have the same operations.
これで,「じゃあserial logとmultiversion logの命令列が全て同じならequivalentじゃん」とはならない.
なぜなら,serial logには$ hを適用できない(適用するとmultiversion logになってしまう)からである.
Serial Log $ Lにおける$ r_i(x) \in Lと,MV Log $ L'における$ r_i(x_j)\in L'は異なる命令である.
なのでもう少し議論する必要がある.
MV Conflict
話を戻すと,2. の中で定義されていたconflictも変わる.
Monoversionでは以下だった(再掲):
(4) all pairs of conflicting operations are $ <related (two operations $ conflict if they operate on the same data item, and at least one is a write).
これがMVだと,
Only one pattern of conflict is possible in an MV log: If $ op_i < op_j and these operations conflict, then $ op_i is $ w_i(x_i) and $ op_j is $ r_j(x_i).
Conflicts of the form $ w_i(x_i) < w_j(x_j) are impossible, because each write produces a new version.
Conflicts of the form $ r_j(x_i) < w_i(x_i)are impossible sinse $ T_jcannot read $ x_iuntil it has been produced.
Thus all conflicts in an MV log correspond to reads-from relationships.
ので,グラフの作り方が変わる.
The serialization graph for MV log is defined as for a regular log.
... Let $ L be an MV log over $ \{T_0, ..., T_n\}. $ SG(L)has nodes $ T_0, ..., T_nand edges $ T_i \to T_j(i\neq j)such that for some $ x,$ T_jreads-x-from $ T_i. That is, $ T_i \to T_jis present iff some $ x, $ r_j(x_i)in an operation of $ L. つまり$ r_j(x_i)を洗い出すだけでグラフが作れる...(言い換えると$ \Sigmaだけでよくて$ <がいらない).
FACT 2. Let $ L and $ L' be MV logs over $ T.
(1) If $ Land $ L'have the same operations, then $ SG(L) = SG(L').
(2) If $ Land $ L'are equivalent, then $ SG(L) = SG(L').
$ r_j(x_i)というとき,この添字(version)まで含めてoperationなので,それが同じなら同じグラフになる.
じゃあ,serial log$ LとMV log$ L'を用意して$ SG(L) = SG(L')ならSerializable,でいいのでは?
と思いがちだが,違う.
なぜなら,(繰り返すが)Serial Log $ Lにおける$ r_i(x) \in Lと,MV Log $ L'における$ r_i(x_j)\in L'は異なる命令である.
ので,serial 1V logにおける$ SGの作り方は未定義のままである.単純に比較する術がない.
さらに,(2)はIfであってiffでない.つまり,「グラフが同じならば等価」とはいえない.
まだまだ議論する必要がある.
One-Copy Serializability
ユーザから見てVersionという概念は透過的である. よって,MV LogだろうとMV Historyだろうと,ユーザから見れば全てのトランザクションについて一つのバージョンしか持っていないように見えて欲しい.
ところが,MV Logではそうならないことがある.
Here is a simple example.
$ w_0(x_0)w_0(y_0)r_1(x_0)w_1(y_1)r_2(y_0)w_2(x_2)
$ T_2reads-y-from $ T_0even though $ T_1comes between $ T_0and $ T_2and produces a new value for $ y. This behavior cannot be reproduced with only one copy of $ y.
これが基本的には問題(serial not-MV logとequivalentにならないこと)の根幹である.
1-Serial
ということで,One-Copyしか持たないデータベースに見えるMV Logというものを定義する.
A serial MV log $ L is one-copy serial(or 1-serial) if for all $ i, j,and $ x, if $ T_jreads-x-from $ T_ithen $ i=j or $ T_iis the last transaction preceding $ T_jthat writes into any version of $ x. ... The log above is not 1-serial, because $ T_2reads-y-from $ T_0, but $ w_0(y_0) < w_1(y_1) < r_2(y_0).
まだどんなMV Logがserial MV Logなのか定義してない.
が,おそらく,serial logをMV logにしたものだと思われる.
つまり,$ \Sigmaにおいて全命令がinterleaveなしで並んでいる,というMV Log.
このserial MV Logは,MVに拡張する際に,読むVersionを選択するので,reads-x-fromが変化してしまう.
それが変化しない条件が1-serialだ,と言っている.
つまり,(それが何であれ)そのタプルについてLast Transactionの書いた値を読む,という縛りを入れれば,One-Copy Serialになる.(というか,One-copy serialとする.)
しかしこの縛りは,結局のところMonoversionにおけるConflictの再来である.先程,
Conflicts of the form $ w_i(x_i) < w_j(x_j) are impossible,
と言ったのに,結局のところ$ <における最後のwriteを読んでいるのだからMVの意味がない.
1-SR
そこで,さらなる広い空間を持つ概念を定義する:
A log is one-copy serializable(or 1-SR) if it is equivalent to a 1-serial log. ... It is possible for a serial log to be 1-SR even though it is not 1-serial itself. For example:
$ w_0(x_0)r_1(x_0)w_1(x_1)r_2(x_0)
is not 1-serial since $ T_2reads-x-from $ T_0instead of $ T_1. But it is 1-SR, because it is equivalent to
$ w_0(x_0)r_2(x_0)r_1(x_0)w_1(x_1).
One-copy serializability is our correctness criterion for multiversion concurrency control.
つまり,1-serialなMV LogとequivalentなMV Logを,1-SRと呼ぶ.
この1-SRはこの論文のキモで,1-SR MV LogならばSerial non-MV Logと等価であることが証明される.
これが,non-MV LogとMV Logの等価性(Equivalence)を議論する道具でもある.
1-SR Equivalence Theorem.
Let $ L be an MV log over $ T. $ L is equivalent to a serial, non-MV log over $ Tiff $ L is 1-SR.
Proof
(If). Let $ L_s, be a 1-serial log equivalent to $ L. Form a serial, non-MV log $ L_s'by translating each $ w_i(x_i) into $ w_i(x) and $ r_i(x_i) into $ r_j(x). Consider any reads-from relationship in $ L_s, say $ T_j reads-x-from $ T_i. Since $ L_s, is 1-serial, no $ w_k(x_k) lies between $ w_i(x_i) and $ r_j(x_i). Hence no $ w_k(x) lies between $ w_i(x) and $ r_j(x) in $ L_s'. Thus, $ T_j reads-x-from $ T_i in $ L_s'. This establishes $ L_s' \equiv L_s. Since $ L_s \equiv L, L \equiv L_s'follows by transitivity (since $ \equiv is an equivalence relation).
(Only if). Let $ L_s' be the hypothesized serial, non-MV log equivalent to $ L.
Translate $ L_s' into a serial MV log $ L_s, by mapping each $ w_i(x) into $ w_i(x_i) and each $ r_j(x) into $ r_j(x_i) such that $ T_j reads-x-from $ T_i in $ L_s'This translation preserves reads-from relationships, so $ L_s \equiv L_s'. By transitivity, $ L \equiv L_s.
It remains to prove that $ L_sis 1-serial. Consider any reads-from relationship in $ L_s', say $ T_j reads-x-from $ T_i. Since $ L_s' is a non-MV log, no $ w_k(x) lies between $ w_i(x)and $ r_i(x). Hence no $ w_k(x_k) lies between $ w_i(x_i) and $ r_j(x_i) in $ L_s,. Thus, $ L_s, is 1-serial, as desired. □
大事なので全て引用する.
Proofについての解説:
(If):
証明しているのは「$ Lが1SRであるならば,$ Lはserial non-MV logとequivalentである」こと.
MV Log$ L,1-serial MV Log $ L_s, さらにserial non-MV Log $ L_s'を用意する.
現段階で$ L \equiv L_sではあるとする.(つまり同じoperationsからなる)
つまりで$ Lは1SR.
さらに,$ L_s'は,$ L_sから単にVersionの添字を削ったものだとする.
# 1-serial logからversionを削ったとき,そのnon-MV logはserialになりうるか?の証明がないな.
# まあ,なりうるのだろうけど.
# serial non-MV logから議論を作りはじめて欲しかった.
$ L_sでは必ず,1-serialの定義通り,writeとreadの間に他のwrite operationは存在しない.
ということは,versionをdropしただけの$ L_s'にも同じことがいえる.
つまり,全てのReadについて,$ L_sで読んでいるVersionを必ず$ L_s'でも読んでいる.
なので$ L_s' \equiv L_s,推移律より$ L \equiv L_s'. (Only If):
証明しているのは「$ Lがserial non-MV logとequivalentであるならば,$ Lは1SRである」こと.
$ L_s'という,$ Lとequivalentなserial non-MV logを仮定する.
$ L_s'をserial MV logに変換する.
$ hとして,$ L_s'と同じwriteを読む,という規則を適用して変換する.
つまり$ L \equiv L_s \equiv L_s'になる.
このとき$ L_sが1-serialであれば,$ Lは1SRであるといえる.
serial non-MV Log$ L_s'は,reads-x-fromの間に他のwriteが含まれない.
これは$ <についての話なので,$ L_sについてもその性質は維持される.
よって$ Lは1-serial.
The 1-Serializability Theorem
1SRの定義はできた.が,あるLog$ Lが1SRかどうかをテストするためには,1-serialなLogを用意する必要がある.
というのでは現実に使い物にならない.
equivalentな1-serial Log$ L'を探索する組み合わせ問題をブルートフォースでやるのではだいぶ苦しいからだ.
そこで,過去のSerializability(2章で解説したもの)のように,Conflictを使ってグラフを描き,循環がなければよし,というロジックにしたい.
厳密には,以下の特性がグラフには欲しい.
1. 同じグラフを生成するLogは,Reads-Fromが同じ
2. トポロジカルソートした際のトランザクションの順序で作ったserial non-MV logも,同じグラフを作る
グラフが非循環 == トポロジカルソート可能 -> serial non MV LogとReads-Fromが同じ == 1SR.という論理.
これがあれば,$ Lでグラフを描いただけで,$ L'が存在するかどうか(1SRかどうか)判定できる.
しかし,1. も2. も証明されていない.とくに,先程$ SG(L)を定義したが,
$ (L \equiv L') \to (SG(L) = SG(L')) は証明されているのに,
$ (SG(L) = SG(L')) \to (L \equiv L')は証明できない.これでは,1. の特性が得られない.
Version Order
前述した,「グラフが同じならログがEquivalent」という特性を得るため,
$ SG(L)に新たな道具(概念)を加える.いわゆるMV(H,<<)とよばれるもの. Given a log $ L and data item $ x, a version order for $ x is any (nonreflexive) total order over all of the versions of $ x written in $ L.
A version order, $ \ll, for $ L is the union of the version orders for all data items.
Given $ L and a version order $ \ll, the multiversion serialization graph, $ MVSG(L, \ll) is $ SG(L)with the following edges added:
(1) for each $ r_k(x_j)and$ w_i(x_i)in $ L, $ k \ne i, if $ x_i \ll x_jthen include $ T_i \to T_j, else include $ T_k \to T_i.
ここはトランザクション処理の理論面,特にMVSRに取り組む人間全てが躓くポイント. 以下典型的なつまづきポイント
1. 同じ言葉が,for ~の部分で違うものを指している.for $ xでは反射律のない全順序(つまり大小)のこと. 2. 記号$ \llは,unionとして定義されるが,$ x_i \ll x_jのように全順序比較の論理記号としても使われている
要するにヤバい.
ともかく,この規則に基づいてエッジを$ SG(L)に追加し,$ MVSG(L,\ll)を作る.
そのexampleを挙げると,以下のようなLog $ L_3について,
https://gyazo.com/09ab64ad26a1da262dc3451e33c8d0ae
Reads-FromについてのGraph $ SG(L_3)は以下
https://gyazo.com/adb8970080848754651acaa243a4c028
これにVersion OrderのEdgeを追加する...つまり,任意のread/writeのペアを取り出し,Version Orderによってエッジを張る.
まず以下のVersion Order $ \llを定義する
https://gyazo.com/e465f0339169b5a0f5d6e3521a8b38fb
このときのMVSG(SGにエッジを追加したもの)は以下:
https://gyazo.com/a725e30b7c4194dea5932b4e16306b26
追加されたエッジは以下:
$ T_0 \to T_4: ... これは規則からはありえないのでは?nikezono.icon
$ T_2 \to T_1: $ r_2(x_0)と$ w_1(x_1)を取り出し,$ x_0 \ll x_1.
$ T_2 \to T_4: ... これもありえない気がするnikezono.icon
$ T_1 \to T_3: $ r_1(z_0)と$ w_3(z_3)を取り出し,$ z_0 \ll z_3.
1-SERIALIZABILITY THEOREM.
An MV log $ L is 1-SR iff there exists a version order $ \llsuch that $ MVSG(L,\ll)is acyclic.
Proof
(If). Let $ L_s be a serial MV log induced by a topological sort of $ MVSG(L, \ll).
That is, $ L_s is formed by topologicahy sorting $ MVSG(L, \ll), and as each node $ T_iis listed in the sort, the operations of $ T_i in $ L are added to $ L_s one by one in any order consistent with $ L. $ L_s has the same operations as $ L, so by Fact 1, $ L \equiv L_s.
It remains to prove that $ L_s, is 1-serial. Consider any reads-from situation, say, $ T_k reads-x-from $ T_j. Let $ w_i(x_i) be any other write on a version of $ x. If $ x_i \ll x_j, then by rule (1) of the MVSG definition, the graph includes $ T_i \to T_j. This edge forces $ T_j to follow $ T_i in $ L_s. If $ x_j \ll x_i, then by rule (l), $ MVSG(L, \ll) includes $ T_k \to T_i. This forces $ T_k to precede $ T_i in $ L_s. In both cases, $ T_i is prevented from falling between $ T_j and $ T_k. Since $ T_i was an arbitrary writer on $ x, this proves that no transaction that writes a version of $ x comes between $ T_j and $ T_k in $ L_s. Thus $ L_s is 1-serial.
(Only if). Given $ L and $ \ll, let $ MV(L, \ll) be the graph specified by statement (1) of the MVSG definition. Statement (1) depends only on the operations in $ Land $ \ll; it does not depend on the order of operations in$ L. Thus, if $ L_1 and $ L_2 are multiversion logs with the same operations, then $ MV(L_1, \ll) = MV(L_2, \ll), for all version orders $ \ll.
Let $ L_s be a 1-serial log equivalent to $ L. All edges in $ SG(L_s) go “left-to-right”, that is, if $ T_i \to T_j, then $ T_i is before $ T_j in $ L_s. Define $ \ll as follows: $ x_i \ll x_j only if $ T_i is before $ T_j in $ L_s. All edges in $ MV( L_s, \ll) are also left-to-right. Therefore ail edges in $ MVSG(L_s, \ll) = MV(L_s, \ll) \cup SG(L_s) are left-to-right, too. This implies that $ MVSG(L_s, \ll) is acyclic.
By Fact 1, $ L and $ L_s have the same operations. Hence, $ MV(L, \ll) = MV(L_s,\ll). By Fact 2, $ SG(L) = SG(L_s). Therefore $ MVSG(L, \ll) = MVSG(L_s, \ll). Since $ MVSG(L_s, \ll)is acyclic, so is $ MVSG(L, \ll). □
解説:
定理: MVSGをが非循環になるような$ \ll(union)が存在するならば,その時に限り$ Lは1SR.
If:
証明したいのは$ MVSG(L,\ll)が非循環ならば必ず$ Lが1SRであること.
まず,MVSGが非循環だと仮定する.と,トポロジカルソートが可能となる.
トポロジカルソートした結果,ノード(トランザクション)の順序集合が作れる
この順序集合の順番そのままで新たにLog$ L_sを作る.
これは,serial MV Logである.(命令がinterleaveされていないから.1-serialとはまだ言っていない)
で,$ Lと同じ命令(versionの添字が同じ)になるようにVersion Function $ hを設定する.
と,同じ命令からなるので,$ L \equiv L_sになる.
あとは,$ L_sが1-serialなら,$ Lは1SRであると結論できる.
1-serialの条件は,あらゆる$ r_k(x_j)について,$ w_j(x_j)との間に他の$ w_i(x_i)が存在しないこと.
ということで$ Lのあらゆるread operation, $ r_k(x_j)について考えてみる.
$ xについての他のwrite operation $ w_i(x_i)すべてについて,$ MVSG(L, \ll)は,Definitionで述べた通りエッジを追加しているはず.
1. $ x_i \ll x_jなら,$ T_i \to T_j
2. $ x_j \ll x_iなら,$ T_k \to T_i
どちらのエッジが張られたにせよ,このエッジをトポロジカルソートして作ったserial MV Log$ L_sは,$ T_jと$ T_kの間に$ T_iを置くことはない.($ T_j \to T_i \to T_kのようなエッジは必ず追加されない)
ということは,$ L_sにおいて$ T_jと$ T_kの間に$ xをwriteしたトランザクションは存在しえない.
よって$ L_sは1-serial.$ L \equiv L_sから,$ Lは1SR.
Only If:
証明したいのは1SRなログ$ Lは必ず$ MVSG(L,\ll)が非循環になる$ \llが存在すること.
MVSGのうち,(1)で描かれるグラフを$ MV(L,\ll)とする.(MVSGからSGを抜いたもの)(FYI: MV(H,<<)) MVを描く上で,$ L上の順序つまり$ <は一切使わないことを考える.
つまり,同じ命令からなる$ SG_1と$ SG_2を考えると,$ MV(L_1, \ll) = MV(L_2, \ll)である.
「あらゆるVersion Order(union) $ \llについてこれがいえる」ことが重要.
同じ命令からなるので,$ SG(L_1) = SG(L_2)でもある
さて,$ Lは1SRなので,equivalentな1-serial logは存在する.これを$ L_sとする.
1-serial ⊂ serial MV logであるから,$ SG(L_s)は非循環である.
非循環で,かつ,serial logであることから,必ず$ L_sの順序$ <に沿ってエッジが引かれていく.
ここで,ある$ \llを考える.これが$ MVSG(L_s, \ll)を非循環たらしめてくれれば,証明が先に進む.
その$ \llは,「$ L_sの順序(つまり$ <にしたがって個々のversion order for $ xを作った」ものとする.
つまり,命令順が来た順とVersion Orderが同じ順序であるとする.
このとき$ MV(L_s, \ll)は全て$ <の順序にならったエッジしかない.
これについては先程述べたように$ SG(L_s)も同じなので,合成した$ MVSG(L_s, \ll)は全てのエッジが$ <に従う.
つまりこういった$ \llを想定すればMVSGが非循環になる.
同じ$ \llを与えたとき,同じ命令からなるLogの間では同じMVを描くことから,$ MVSG(L_s, \ll) = MVSG(L, \ll)
で,前者が非循環なので,後者も非循環.
さて,ここまでやったが,
1-SR COMPLEXITY THEOREM.
It is NP-Complete to decide whether an MV log is 1-SR.
証明の引用は省く.
あるログ$ Lがあったとして,それと同じ命令からなる1-serialなログ$ L_sが必要になる.
同じ命令からなる1-serialなログを用意する手立てがないのでNon-deterministic P.
MVSGを描くにも$ \llが必要なのだが,この$ \llの取りうるパターンも指数的に多い.
1-serialなログか,何らかの$ \llがあればPで検証できる,ということでNP-Complete.
結局,あるログが1SRかどうか調べる方法はSERIALIZABILITY THEOREMで提供されたが,
その計算量はNP完全だった.つまりオンラインで解くには実用にならない.
4章以降について
以降は解説しない...というか読んでない.その理由(つまり言い訳)を下に書く.
以降の章は,全て
既存のMultiversion Concurrency Control Protcolが1SRを満たすこと
また,同時に,1SRだが2章で説明した(Old) Serializabilityを満たさないこと
の説明をしている.
4章で MVTOという手法,5章でMV2PLという手法,6章ではPrime社が当時開発したプロトコルの解説をしている. 私見だが,このような実例ベースの説明(ある手法が1SRを満たすこと)の説明はあまり意味がないと感じるし,
MVTOも含めてほとんど実用されているプロトコルではないので,読み飛ばした.
本質的に重要なのは,1SRを満たす手法こそが(また,それのみに限り)MultiversionにおけるSerializablityを持つ,ということの定理と証明であると思う.
この定理と証明をexploitsして,新たな手法が生まれていくことを祈りたい.(がすでに30年以上経っている)